The present application relates generally to an improved data processing apparatus and method and more specifically to mechanisms for efficient redundancy identification, redundancy removal, and sequential equivalence checking within designs including memory arrays.
Formal and semiformal verification techniques are powerful tools for the construction of correct logic designs. They have the power to expose even the most probabilistically uncommon scenario that may result in a functional design failure, and ultimately have the power to prove that the design is correct, i.e. that no failing scenario exists. Unfortunately, formal verification techniques require computational resources that are exponential with respect to the size of the design under test. Semiformal verification techniques leverage formal algorithms to larger designs by applying them only in a resource-bounded manner, though at the expense of incomplete verification coverage.
U.S. Pat. No. 6,698,003 proposes the generic concept of “transformation-based verification” to enable the use of multiple algorithms, encapsulated as “engines” of a modular multiple-engine based verification system to synergistically simplify and decompose complex problems into simpler sub-problems that are easier to formally discharge. The transformation-based verification paradigm has demonstrated itself essential to enhance the scalability of formal verification algorithms to verification problems of industrial relevance, where it is often desired to leverage the bug-hunting power of formal methods to large units of logic that are the common focus of simulation-based test benches.
One large capacity gap between traditional formal verification algorithms vs. simulation-based testbenches is due to bit-blasting employed in the. In particular, virtually every industrial hardware formal verification tool “bit-blasts” design components into simpler primitives, such as two-input AND gates, inverters, and single-bit state elements. In contrast, logic simulators often support higher-level primitives without bit-blasting. One type of design component that often entails a dramatic bloat when bit-blasted is a memory array, which is a row-addressable, two-dimensional state element often used to represent main memory or caches. Such memory arrays may be extremely large when bit-blasted. Modern caches often are several megabytes, and if verifying a design component that interacts with main memory, it may even be required to support more than 232 rows of arbitrary width. Bit-blasting of such large memory arrays often constitutes a fatal bottleneck to formal verification tools.
Logic designs used to represent hardware, software, or hybrid systems may be represented using a variety of formats. Example formats include hardware description languages (HDLs), higher-level languages such as SystemC, or lower-level formats such as netlists. There are numerous application domains in which it is advantageous to reduce the size of design representations. For example, logic synthesis and design aids often attempt to yield more compact representations that lend themselves to higher quality silicon or assembly code.
Verification frameworks, such as logic simulators and accelerators, often dramatically benefit in speed and capacity from techniques to reduce the size of the corresponding logic representation. Equivalence checking frameworks, pervasively used in the semiconductor industry to establish the behavioral equivalence of two versions of a design, often are critically sensitive to the ability to reduce the size of the composition of the two designs to adequately scale to the desired magnitude. Various design debug, visualization, and coverage analysis tools attempt to build more abstract views of a logic representation. These tools often represent memory arrays, which are common components in many types of logic designs, at quite a low level of abstraction. These tools represent custom logic design components including aspects, such as test and reliably features.